\begin{tabbing}
($\backslash$p. let\= x, y = dest\_sqequal (h ({-}1) p) in \+
\\[0ex](\=Assert (mk\_equal\_term bool\_term y y)\+
\\[0ex]
\\[0ex]THENL [(Auto\_aux (first\_nat 1:n) ((first\_nat 1:n),(first\_nat 3:n)) (first\_tok 
\-\-\\[0ex]:t) inil\_term); SqSubs\=tAtAddr [2] x ({-}1) \+
\\[0ex]THENL [
\-\\[0ex](Auto\_aux (first\_nat 1:n) ((first\_nat 1:n),(first\_nat 4:n)) (first\_tok :t) inil\_term)
\\[0ex]; Id]]) p)
\end{tabbing}